| 1: | minus_active(0,y) | → 0 | |
| 2: | mark(0) | → 0 | |
| 3: | minus_active(s(x),s(y)) | → minus_active(x,y) | |
| 4: | mark(s(x)) | → s(mark(x)) | |
| 5: | ge_active(x,0) | → true | |
| 6: | mark(minus(x,y)) | → minus_active(x,y) | |
| 7: | ge_active(0,s(y)) | → false | |
| 8: | mark(ge(x,y)) | → ge_active(x,y) | |
| 9: | ge_active(s(x),s(y)) | → ge_active(x,y) | |
| 10: | mark(div(x,y)) | → div_active(mark(x),y) | |
| 11: | div_active(0,s(y)) | → 0 | |
| 12: | mark(if(x,y,z)) | → if_active(mark(x),y,z) | |
| 13: | div_active(s(x),s(y)) | → if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0) | |
| 14: | if_active(true,x,y) | → mark(x) | |
| 15: | minus_active(x,y) | → minus(x,y) | |
| 16: | if_active(false,x,y) | → mark(y) | |
| 17: | ge_active(x,y) | → ge(x,y) | |
| 18: | if_active(x,y,z) | → if(x,y,z) | |
| 19: | div_active(x,y) | → div(x,y) | |
| 20: | MINUS_ACTIVE(s(x),s(y)) | → MINUS_ACTIVE(x,y) | |
| 21: | MARK(s(x)) | → MARK(x) | |
| 22: | MARK(minus(x,y)) | → MINUS_ACTIVE(x,y) | |
| 23: | MARK(ge(x,y)) | → GE_ACTIVE(x,y) | |
| 24: | GE_ACTIVE(s(x),s(y)) | → GE_ACTIVE(x,y) | |
| 25: | MARK(div(x,y)) | → DIV_ACTIVE(mark(x),y) | |
| 26: | MARK(div(x,y)) | → MARK(x) | |
| 27: | MARK(if(x,y,z)) | → IF_ACTIVE(mark(x),y,z) | |
| 28: | MARK(if(x,y,z)) | → MARK(x) | |
| 29: | DIV_ACTIVE(s(x),s(y)) | → IF_ACTIVE(ge_active(x,y),s(div(minus(x,y),s(y))),0) | |
| 30: | DIV_ACTIVE(s(x),s(y)) | → GE_ACTIVE(x,y) | |
| 31: | IF_ACTIVE(true,x,y) | → MARK(x) | |
| 32: | IF_ACTIVE(false,x,y) | → MARK(y) | |